For two given $\omega$-terms $\alpha$ and $\beta$, the word problem for$\omega$-terms over a variety $\boldsymbol{\mathrm{V}}$ asks whether$\alpha=\beta$ in all monoids in $\boldsymbol{\mathrm{V}}$. We show that theword problem for $\omega$-terms over each level of the Trotter-Weil Hierarchyis decidable. More precisely, for every fixed variety in the Trotter-WeilHierarchy, our approach yields an algorithm in nondeterministic logarithmicspace (NL). In addition, we provide deterministic polynomial time algorithmswhich are more efficient than straightforward translations of theNL-algorithms. As an application of our results, we show that separability bythe so-called corners of the Trotter-Weil Hierarchy is witnessed by$\omega$-terms (this property is also known as $\omega$-reducibility). Inparticular, the separation problem for the corners of the Trotter-WeilHierarchy is decidable.
展开▼
